% David Vega and Stan Warford
% Pepperdine University
% File: Vega-Equations
% !TEX TS-program = xelatex

\documentclass[12pt, fleqn, leqno]{article}

\usepackage{times}
\usepackage{amsmath, amsthm, amssymb,latexsym}
\usepackage{wasysym}                                % For temporal operators, Diamond and Box
\usepackage{eucal}                                  % For temporal operators, Until and Wait

%\linespread{0.1}
%\setlength{\parskip}{-10pt plus 0pt minus 0pt}


\newcommand{\lgap}{2pt}                             % Line gap
\newcommand{\llgap}{6pt}                            % Larger line gap
\newcommand{\lllgap}{32pt}                          % Largest line gap for students to write in
\newcommand{\mymathindent}{24pt}                    % Indentation for math tabbing
\newcommand{\equivs}{\ensuremath{\;\equiv\;}}       % Equivales with space
\newcommand{\equivss}{\ensuremath{\;\;\equiv\;\;}}  % Equivales with double space
\newcommand{\nequiv}{\ensuremath{\not\equiv}}       % Inequivalent
\newcommand{\impl}{\ensuremath{\Rightarrow}}        % Implies
\newcommand{\nimpl}{\ensuremath{\not\Rightarrow}}   % Does not imply
\newcommand{\foll}{\ensuremath{\Leftarrow}}         % Follows from
\newcommand{\nfoll}{\ensuremath{\not\Leftarrow}}    % Does not follow from

% Macros for Temporal Operators
\newcommand{\Until}{\;\mathcal{U}\;}
\newcommand{\Wait}{\;\mathcal{W}\;}
\newcommand{\Next}{\;\,\text{\raisebox{3.5pt}{\circle{6}}}}
\newcommand{\Event}{\Diamond\,}
\newcommand{\Always}{\Box\,}

\newcommand{\myqed}{\hfill\rule[-.23ex]{1.2ex}{2.0ex}}
\newcommand{\spacer}{\vspace{-30pt}}
\newcommand{\firstspacer}{\vspace{-26pt}}

% Thanks to David Gries for sharing the following macros
% Macros for quantifications.
\newcommand{\thedr}{\rule[-.25ex]{.32mm}{1.75ex}}   % Symbol that separates dummy from range in quantification
\newcommand{\dr}{\;\,\thedr\,\;}                    % Symbol that separates dummy from range, with spacing
\newcommand{\rb}{:}                                 % Symbol that separates range from body in quantification
\newcommand{\drrb}{\;\thedr\,{:}\;}                 % Symbol that separates dummy from body when range is missing
\newcommand{\all}{\forall}                          % Universal quantification
\newcommand{\ext}{\exists}                          % Existential quantification


% Macros for proof hints
\newcommand{\Gll} {\langle}                         % Open hint
\newcommand{\Ggg} {\rangle}                         % Close hint
\newlength{\Glllength}                              % Length of open hint symbol
\settowidth{\Glllength}{$.\Gll$}
\newcommand{\Hint}[1]     {\ \ \ $\Gll              \mbox{#1} \Ggg$ }   % Single line hint
\newcommand{\Hintfirst}[1]{\ \ \ $\Gll              \mbox{#1}$ }        % First line of multiline hint
\newcommand{\Hintmid}[1]  {\ \ $\hspace{\Glllength} \mbox{#1}$ }        % Middle line of multiline hint
\newcommand{\Hintlast}[1] {\ \ $\hspace{\Glllength} \mbox{#1} \Ggg$ }   % Last line of multiline hint


% Single and double quotes
\newcommand{\Lq}{\mbox{`}}
\newcommand{\Rq}{\mbox{'}}
\newcommand{\Lqq}{\mbox{``}}
\newcommand{\Rqq}{\mbox{''}}

\oddsidemargin  0.0in
\evensidemargin 0.0in
\textwidth      6.0in
\headheight     0.0in
\topmargin      0.0in
\textheight=8.5in
\parindent=0in
%\pagestyle{plain}

\pagestyle{myheadings} 
\markboth{\textbf{Draft} \today} {\textbf{Draft} \today}

\title{Theorems from Vega and Warford's EDS4LTL\\(Draft)}

\author{David Vega\thanks{Research supported by Tooma Undergraduate Research Fellowship Program, Summer 2009}\\
   J. Stanley Warford\\
   Computer Science Department\\
   Pepperdine University\\
   Malibu, CA 90265}
\date{} % Required for no date to appear in heading

\begin{document}

\maketitle

\begin{abstract}
The first section of this document is a collection of the axioms and theorems of the
propositional calculus in Gries and Schneider's
book \textit{A Logical Approach to Discrete Math}, Springer-Verlag, 1993 (LADM).
The numbering is consistent with that text with the chapter number followed by the equation number separated by a period.
Additional theorems, either not included in LADM or included but not numbered, are indicated by a three-part number with two period separators.
The second section is a collection of the axioms and theorems of linear temporal logic
in Vega and Warford's paper \textit{An Equational Deductive System for Linear Temporal Logic}
(EDS4LTL),
Pepperdine University Research Report, Natural Science Division, 2015.
\end{abstract}

\subsection*{Table of Precedences}

%\setlength\extrarowheight{2pt}
\begin{tabular}{lr}
\hline
$[x := e]$ (textual substitution) & Highest precedence\\
$\neg$\quad $\Next$\quad $\Event$\quad $\Always$ &\\
$\Until$\quad $\Wait$ &\\
$=$\quad (conjunctional) &\\
$\lor$\quad $\land$ &\\
$\impl$\quad $\foll$ &\\
$\equiv$ \quad (associative) & Lowest precedence\\
\hline
\end{tabular}\\[\llgap]

\section*{Theorems of the Propositional Calculus}

\subsection*{Equivalence and $true$}
\begin{tabbing}
(99.99.9)\;\=\kill
(3.1)\>\textbf{Axiom, Associativity of $\equiv$ :}\quad $((p\equiv q) \equiv r)\equivs (p\equiv (q\equiv r))$\\[\lgap]
(3.2)\>\textbf{Axiom, Symmetry of $\equiv$ :}\quad $p\equiv q \equiv q\equiv p$\\[\lgap]
(3.3)\>\textbf{Axiom, Identity of $\equiv$ :}\quad $true\equiv q \equiv q$\\[\lgap]
(3.4)\>$true$\\[\lgap]
(3.5)\>\textbf{Reflexivity of $\equiv$ :}\quad $p\equiv p$\\
\end{tabbing}

\subsection*{Negation, inequivalence, and $false$}
\begin{tabbing}
(99.99.9)\;\=\kill
(3.8)\>\textbf{Definition of $false$ :}\quad $false\equiv \neg true$\\[\lgap]
(3.9)\>\textbf{Axiom, Distributivity of $\neg$ over $\equiv$ :}\quad $\neg (p\equiv q) \equivs \neg p \equiv q$\\[\lgap]
(3.10)\>\textbf{Definition of $\nequiv$ :}\quad $(p\nequiv q)\equivs\neg(p\equiv q)$\\[\lgap]
(3.11)\>$\neg p \equiv q \equiv p \equiv \neg q$\\[\lgap]
(3.12)\>\textbf{Double negation:}\quad $\neg\neg p\equiv p$\\[\lgap]
(3.13)\>\textbf{Negation of $false$:}\quad $\neg false\equiv true$\\[\lgap]
(3.14)\>$(p\nequiv q)\equivs\neg p\equiv q$\\[\lgap]
(3.15)\>$\neg p\equiv p\equiv false$\\[\lgap]
(3.16)\>\textbf{Symmetry of $\nequiv$ :}\quad $(p\nequiv q) \equivs (q\nequiv p)$\\[\lgap]
(3.17)\>\textbf{Associativity of $\nequiv$ :}\quad $((p\nequiv q) \nequiv r)\equivs (p\nequiv (q\nequiv r))$\\[\lgap]
(3.18)\>\textbf{Mutual associativity:}\quad $((p\nequiv q) \equiv r)\equivs (p\nequiv (q\equiv r))$\\[\lgap]
(3.19)\>\textbf{Mutual interchangeability:}\quad $p\nequiv q \equiv r\equivss p\equiv q\nequiv r$\\
(3.19.1)\>$p\nequiv p \nequiv q\equivs q$\\
\end{tabbing}

\subsection*{Disjunction}
\begin{tabbing}
(99.99.9)\;\=\kill
(3.24)\>\textbf{Axiom, Symmetry of $\lor$ :}\quad $p\lor q \equiv q\lor p$\\[\lgap]
(3.25)\>\textbf{Axiom, Associativity of $\lor$ :}\quad $(p\lor q) \lor r\equiv p\lor (q\lor r)$\\[\lgap]
(3.26)\>\textbf{Axiom, Idempotency of $\lor$ :}\quad $p\lor p \equiv p$\\[\lgap]
(3.27)\>\textbf{Axiom, Distributivity of $\lor$ over $\equiv$ :}\quad $p\lor (q\equiv r)\equiv p\lor q\equiv p\lor r$\\[\lgap]
(3.28)\>\textbf{Axiom, Excluded middle:}\quad $p\lor\neg p$\\[\lgap]
(3.29)\>\textbf{Zero of $\lor$ :}\quad $p\lor true\equiv true$\\[\lgap]
(3.30)\>\textbf{Identity of $\lor$ :}\quad $p\lor false\equiv p$\\[\lgap]
(3.31)\>\textbf{Distributivity of $\lor$ over $\lor$ :}\quad $p\lor (q\lor r)\equiv (p\lor q)\lor (p\lor r)$\\[\lgap]
(3.32)\>$p\lor q\equiv p\lor\neg q\equiv p$\\
\end{tabbing}

%\newpage

\subsection*{Conjunction}
\begin{tabbing}
(99.99.9)\;\=(m)\;\=\kill
(3.35)\>\textbf{Axiom, Golden rule:}\quad $p\land q\equivs p\equivs q\equivs p\lor q$\\[\lgap]
(3.36)\>\textbf{Symmetry of $\land$ :}\quad $p\land q \equiv q\land p$\\[\lgap]
(3.37)\>\textbf{Associativity of $\land$ :}\quad $(p\land q) \land r\equiv p\land (q\land r)$\\[\lgap]
(3.38)\>\textbf{Idempotency of $\land$ :}\quad  $p\land p \equiv p$\\[\lgap]
(3.39)\>\textbf{Identity of $\land$ :}\quad $p\land true\equiv p$\\[\lgap]
(3.40)\>\textbf{Zero of $\land$ :}\quad $p\land false\equiv false$\\[\lgap]
(3.41)\>\textbf{Distributivity of $\land$ over $\land$ :}\quad $p\land (q\land r)\equiv (p\land q)\land (p\land r)$\\[\lgap]
(3.42)\>\textbf{Contradiction:}\quad $p \land \neg p \equiv false$\\[\lgap]
(3.43)\>\textbf{Absorption:}\\
      \> (a)\> $p \land (p \lor q) \equiv p$\\[\lgap]
      \> (b)\> $p \lor (p \land q) \equiv p$\\[\lgap]
(3.44)\>\textbf{Absorption:}\\
      \> (a)\> $p \land (\neg p \lor q) \equiv p \land q$\\[\lgap]
      \> (b)\> $p \lor (\neg p \land q) \equiv p \lor q$\\[\lgap]
(3.45)\>\textbf{Distributivity of $\lor$ over $\land$ :}\quad $p\lor (q\land r)\equiv (p\lor q)\land (p\lor r)$\\[\lgap]
(3.46)\>\textbf{Distributivity of $\land$ over $\lor$ :}\quad $p\land (q\lor r)\equiv (p\land q)\lor (p\land r)$\\[\lgap]
(3.47)\>\textbf{De Morgan:}\\
      \> (a)\> $\neg (p \land q) \equiv \neg p \lor \neg q$\\[\lgap]
      \> (b)\> $\neg (p \lor q) \equiv \neg p \land \neg q$\\[\lgap]
(3.48)\>$p\land q\equivs p\land \neg q\equivs \neg p$\\[\lgap]
(3.49)\>$p\land (q\equiv r)\equivs p\land q\equivs p\land r \equivs p$\\[\lgap]
(3.50)\>$p\land (q\equiv p)\equivs p\land q$\\[\lgap]
(3.51)\>\textbf{Replacement:}\quad $(p \equiv q) \land (r \equiv p) \equivss (p \equiv q) \land (r \equiv q)$\\[\lgap]
(3.52)\>\textbf{Equivalence:}\quad $p \equiv q \equivs (p \land q) \lor (\neg p \land \neg q)$\\[\lgap]
(3.53)\>\textbf{Exclusive or:}\quad $p \nequiv q \equivs (\neg p \land q) \lor (p \land \neg q)$\\[\lgap]
(3.55)\>$(p\land q)\land r \equivs p \equivs q \equivs r \equivs p\lor q \equivs q\lor r \equivs r\lor p \equivs p \lor q\lor r$\\
\end{tabbing}

%\newpage

\subsection*{Implication}
\begin{tabbing}
(99.99.9)\;\=(m)\;\=\kill
(3.57)\>\textbf{Definition of Implication:}\quad $p\impl q \equivs p\lor q \equivs q$\\[\lgap]
(3.58)\>\textbf{Axiom, Consequence:}\quad $p\foll q \equivs q\impl p$\\[\lgap]
(3.59)\>\textbf{Implication:}\quad $p\impl q \equivs \neg p \lor q$\\[\lgap]
(3.60)\>\textbf{Implication:}\quad $p\impl q \equivs p\land q \equivs p$\\[\lgap]
(3.61)\>\textbf{Contrapositive:}\quad $p\impl q \equivs \neg q\impl \neg p$\\[\lgap]
(3.62)\>$p\impl (q\equiv r) \equivs p\land q\equivs p\land r$\\[\lgap]
(3.63)\>\textbf{Distributivity of $\impl$ over $\equiv$ :}\quad $p\impl (q\equiv r)\equivs (p\impl q)\equivs (p\impl r)$\\[\lgap]
(3.64)\>$p\impl (q\impl r) \equivs (p\impl q)\impl (p\impl r)$\\[\lgap]
(3.65)\>\textbf{Shunting:}\quad $p\land q\impl r\equivs p\impl (q\impl r)$\\[\lgap]
(3.66)\>$p\land (p\impl q) \equivs p\land q$\\[\lgap]
(3.67)\>$p\land (q\impl p) \equivs p$\\[\lgap]
(3.68)\>$p\lor (p\impl q) \equivs true$\\[\lgap]
(3.69)\>$p\lor (q\impl p) \equivs q\impl p$\\[\lgap]
(3.70)\>$p\lor q \impl p\land q \equivs p \equivs q$\\[\lgap]
(3.71)\>\textbf{Reflexivity of $\impl$ :}\quad $p\impl p$\\[\lgap]
(3.72)\>\textbf{Right zero of $\impl$ :}\quad $p\impl true \equivs true$\\[\lgap]
(3.73)\>\textbf{Left identity of $\impl$ :}\quad $true\impl p \equivs p$\\[\lgap]
(3.74)\>$p\impl false \equivs \neg p$\\[\lgap]
(3.74.1)\>$\neg p\impl false \equivs p$\\[\lgap]
(3.75)\>$false\impl p \equivs true$\\[\lgap]
(3.76)\>\textbf{Weakening/strengthening:}\\
      \> (a)\> $p\impl p\lor q$\quad \quad \quad (Weakening the consequent)\\[\lgap]
      \> (b)\> $p\land q \impl p$\quad \quad \quad (Strengthening the antecedent)\\[\lgap]
      \> (c)\> $p\land q \impl p\lor q$\quad \quad \quad (Weakening/strengthening)\\[\lgap]
      \> (d)\> $p\lor (q\land r) \impl p\lor q$\\[\lgap]
      \> (e)\> $p\land q \impl p\land (q \lor r)$\\[\lgap]
(3.76.1)\>$p\land q \impl p\lor r$\quad \quad \quad (Weakening/strengthening)\\[\lgap]
(3.76.2)\>$(p\impl q) \impl ((q\impl r)\impl (p\impl r))$\\[\lgap]
(3.77)\>\textbf{Modus ponens:}\quad $p\land (p\impl q)\impl q$\\[\lgap]
(3.77.1)\>\textbf{Modus tollens:}\quad $(p\impl q)\land \neg q \impl \neg p$\\[\lgap]
(3.78)\>$(p\impl r) \land (q\impl r) \equivs (p\lor q\impl r)$\\[\lgap]
(3.79)\>$(p\impl r) \land (\neg p\impl r) \equivs r$\\[\lgap]
(3.80)\>\textbf{Mutual implication:}\quad $(p\impl q) \land (q\impl p) \equivs (p\equiv q)$\\[\lgap]
(3.81)\>\textbf{Antisymmetry:}\quad $(p\impl q) \land (q\impl p) \impl (p\equiv q)$\\[\lgap]
(3.82)\>\textbf{Transitivity:}\\
      \> (a)\> $(p\impl q) \land (q\impl r) \impl (p\impl r)$\\[\lgap]
      \> (b)\> $(p\equiv q) \land (q\impl r) \impl (p\impl r)$\\[\lgap]
      \> (c)\> $(p\impl q) \land (q\equiv r) \impl (p\impl r)$\\[\lgap]
(3.82.1)\>\textbf{Transitivity of $\equiv$ :}\quad $(p\equiv q)\land (q\equiv r)\impl (p\equiv r)$\\[\lgap]
(3.82.2)\>$(p\equiv q)\impl (p\impl q)$\\
\end{tabbing}

\newpage

\subsection*{Leibniz as an axiom}
\begin{tabbing}
(99.99.9)\;\=(m)\;\=\kill
This section uses the following notation: $E^{z}_{X}$ means $E[z := X]$.\\[\lgap]
(3.83)\>\textbf{Axiom, Leibniz:}\quad $e=f\impl E^{z}_{e} = E^{z}_{f}$\\[\lgap]
(3.84)\>\textbf{Substitution:}\\
      \> (a)\> $(e=f) \land E^{z}_{e} \equivs (e=f)\land E^{z}_{f}$\\[\lgap]
      \> (b)\> $(e=f) \impl E^{z}_{e} \equivs (e=f)\impl E^{z}_{f}$\\[\lgap]
      \> (c)\> $q\land (e=f) \impl E^{z}_{e} \equivs q\land (e=f)\impl E^{z}_{f}$\\[\lgap]
(3.85)\>\textbf{Replace by $true$:}\\
      \> (a)\> $p \impl E^{z}_{p} \equivs p\impl E^{z}_{true}$\\[\lgap]
      \> (b)\> $q\land p \impl E^{z}_{p} \equivs q\land p\impl E^{z}_{true}$\\[\lgap]
(3.86)\>\textbf{Replace by $false$:}\\
      \> (a)\> $E^{z}_{p} \impl p \equivs E^{z}_{false}\impl p$\\[\lgap]
      \> (b)\> $E^{z}_{p} \impl p\lor q \equivs E^{z}_{false}\impl p\lor q$\\[\lgap]
(3.87)\>\textbf{Replace by $true$:}\quad $p\land E^{z}_{p} \equivs p\land E^{z}_{true}$\\[\lgap]
(3.88)\>\textbf{Replace by $false$:}\quad $p\lor E^{z}_{p} \equivs p\lor E^{z}_{false}$\\[\lgap]
(3.89)\>\textbf{Shannon:}\quad $E^{z}_{p}\equivs (p\land E^{z}_{true}) \lor (\neg p\land E^{z}_{false})$\\
\end{tabbing}

\subsection*{Additional theorems concerning implication}
\begin{tabbing}
(99.99.9)\;\=(m)\;\=\kill
(4.1)\>$p\impl (q\impl p)$\\[\lgap]
(4.2)\>\textbf{Monotonicity of $\lor$ :}\quad $(p\impl q) \impl (p\lor r \impl q\lor r)$\\[\lgap]
(4.3)\>\textbf{Monotonicity of $\land$ :}\quad $(p\impl q) \impl (p\land r \impl q\land r)$\\[\lgap]
\end{tabbing}

\subsection*{Proof technique metatheorems.}
\begin{tabbing}
(99.99.9)\;\=(m)\;\=\kill
(4.4)\>\textbf{Deduction (assume conjuncts of antecedent):}\\[\lgap]
      \>To prove $P_{1}\land P_{2}\impl Q$, assume $P_{1}$ and $P_{2}$, and prove $Q$.\\[\lgap]
      \>You cannot use textual substitution in $P_{1}$ or $P_{2}$.\\[\lgap]
(4.5)\>\textbf{Case analysis:}\quad If $E^{z}_{true}$ and $E^{z}_{false}$ are theorems, then so is $E^{z}_{P}$.\\[\lgap]
(4.6)\>\textbf{Case analysis:}\quad $(p\lor q\lor r)\land (p\impl s)\land (q\impl s)\land (r\impl s)\impl s$\\[\lgap]
(4.7)\>\textbf{Mutual implication:}\quad To prove $P\equiv Q$, prove $P\impl Q$ and $Q\impl P$.\\[\lgap]
(4.7.1)\>\textbf{Truth implication:}\quad To prove $P$, prove $true\impl P$.\\[\lgap]
(4.9)\>\textbf{Proof by contradiction:}\quad To prove $P$, prove $\neg P\impl false$.\\[\lgap]
(4.12)\>\textbf{Proof by contrapositive:}\quad To prove $P\impl Q$, prove $\neg Q\impl \neg P$.\\
\end{tabbing}

\newpage

\section*{Theorems of Linear Temporal Logic}

\subsection*{Next $\quad\Next$}

\begin{equation}\label{E:selfDual}
\textbf{Axiom, Self-dual:}\quad \Next\neg p \equiv \neg\Next p
\end{equation}

\firstspacer

\begin{equation}\label{E:distNextImp}
\textbf{Axiom, Distributivity of $\Next$ over $\impl$:}\quad \Next (p \impl q) \equiv \Next p \impl \Next q
\end{equation}

\spacer

\begin{equation}\label{E:linearity}
\textbf{Linearity:}\quad \Next p \equiv \neg\Next\neg p
\end{equation}

\spacer

\begin{equation}\label{E:distNextOr}
\textbf{Distributivity of $\Next$ over $\lor$:}\quad \Next (p \lor q) \equiv \Next p \lor \Next q
\end{equation}

\spacer

\begin{equation}\label{E:distNextAnd}
\textbf{Distributivity of $\Next$ over $\land$:}\quad \Next (p \land q) \equiv \Next p \land \Next q
\end{equation}

\spacer

\begin{equation}\label{E:distNextEquiv}
\textbf{Distributivity of $\Next$ over $\equiv$:}\quad \Next (p \equiv q) \equiv \Next p \equiv \Next q
\end{equation}

\spacer

\begin{equation}\label{E:nextTruth}
\textbf{Truth of $\Next$:}\quad \Next true \equiv true
\end{equation}

\spacer

\begin{equation}\label{E:nextFalse}
\textbf{Falsehood of $\Next$:}\quad \Next false \equiv false
\end{equation}

\subsection*{Until $\quad\Until$}

\begin{equation}\label{E:distNextUntil}
\textbf{Axiom, Distributivity of $\Next$ over $\Until$:}\quad \Next (p \Until q) \equiv \Next p \Until \Next q
\end{equation}

\firstspacer

\begin{equation}\label{E:expansionUntil}
\textbf{Axiom, Expansion of $\Until$:}\quad p \Until q \equiv q \lor (p \land \Next (p \Until q))
\end{equation}

\spacer

\begin{equation}\label{E:untilFalse}
\textbf{Axiom, Right zero of $\Until$:}\quad p \Until false \equiv false
\end{equation}

\spacer

\begin{equation}\label{E:untilOrEquiv}
\textbf{Axiom, Left distributivity of $\Until$ over $\lor$ :}\quad p \Until (q \lor r) \equiv p \Until q \lor p \Until r
\end{equation}

\spacer

\begin{equation}\label{E:untilOrImp}
\textbf{Axiom, Right distributivity of $\Until$ over $\lor$ :}\quad p \Until r \lor q \Until r \impl (p \lor q) \Until r
\end{equation}

\spacer

\begin{equation}\label{E:untilAndImp}
\textbf{Axiom, Left distributivity of $\Until$ over $\land$ :}\quad p \Until (q \land r) \impl p \Until q \land p \Until r
\end{equation}

\spacer

\begin{equation}\label{E:untilAndEquiv}
\textbf{Axiom, Right distributivity of $\Until$ over $\land$ :}\quad (p \land q) \Until r \equiv p \Until r \land q \Until r
\end{equation}

\spacer

\begin{equation}\label{E:untilIdem}
\textbf{Axiom, Left absorption of $\Until$:}\quad p \Until (p \Until q) \equiv p \Until q
\end{equation}

\spacer

\begin{equation}\label{E:untilIdemR}
\textbf{Axiom, Right absorption of $\Until$:}\quad (p \Until q) \Until q \equiv p \Until q
\end{equation}

\spacer

\begin{equation}\label{E:untilExcludedMiddle}
\Until \textbf{excluded middle:}\quad p \Until q \lor p\Until \neg q
\end{equation}

\spacer

\begin{equation}\label{E:idemUntil}
\textbf{Idempotency of $\Until$:}\quad p \Until p \equiv p
\end{equation}

\spacer

\begin{equation}\label{E:zeroUntil}
\textbf{Right zero of $\Until$:}\quad p \Until true \equiv true
\end{equation}

\spacer

\begin{equation}\label{E:leftIdUntil}
\textbf{Left identity of $\Until$:}\quad false \Until q \equiv q
\end{equation}

\spacer

\begin{equation}\label{E:untilImpOr}
p \Until q \impl p \lor q
\end{equation}

\spacer

\begin{equation}\label{E:untilInsertion}
\textbf{Insertion:}\quad q \impl p \Until q
\end{equation}

\spacer

\begin{equation}\label{E:untilOrP}
\textbf{Absorption:}\quad p \lor p \Until q \equiv p \lor q
\end{equation}

\spacer

\begin{equation}\label{E:untilOrQ}
\textbf{Absorption:}\quad p \Until q \lor q \equiv p \Until q
\end{equation}

\spacer

\begin{equation}\label{E:untilAndQ}
\textbf{Absorption:}\quad p \Until q \land q \equiv q
\end{equation}

\spacer

\begin{equation}\label{E:untilAndOr}
\textbf{Absorption:}\quad p \Until q \land (p \lor q) \equiv p \Until q
\end{equation}

\spacer

\begin{equation}\label{E:untilOrAnd}
\textbf{Absorption:}\quad p \Until q \lor (p \land q) \equiv p \Until q
\end{equation}

\newpage

\subsection*{Eventually $\quad\Event$}

\begin{equation}\label{E:defEvent}
\textbf{Definition of $\Event$:}\quad \Event q \equiv true \Until q
\end{equation}

\firstspacer

\begin{equation}\label{E:absEventIntoUntil}
\textbf{Absorption of $\Event$ into $\Until$:}\quad p \Until q\land \Event q \equiv p\Until q
\end{equation}

\spacer

\begin{equation}\label{E:eventuality}
\textbf{Eventuality:}\quad p \Until q \impl \Event q
\end{equation}

\spacer

\begin{equation}\label{E:eventTrue}
\textbf{Truth of $\Event$:}\quad \Event true \equiv true
\end{equation}

\spacer

\begin{equation}\label{E:eventFalse}
\textbf{Falsehood of $\Event$:}\quad \Event false \equiv false
\end{equation}

\spacer

\begin{equation}\label{E:expansionEvent}
\textbf{Expansion of $\Event$:}\quad \Event p \equiv p \lor \Next\Event p
\end{equation}

\spacer

\begin{equation}\label{E:absOrIntoEvent}
\textbf{Absorption of $\lor$ into $\Event$:}\quad p \lor \Event p \equiv \Event p
\end{equation}

\spacer

\begin{equation}\label{E:absEventIntoAnd}
\textbf{Absorption of $\Event$ into $\land$:}\quad \Event p \land p \equiv p
\end{equation}

\spacer

\begin{equation}\label{E:impEvent}
\textbf{Weakening of $\Event$:}\quad p \impl \Event p
\end{equation}

\spacer

\begin{equation}\label{E:nextEvent}
\textbf{Weakening of $\Event$:}\quad \Next p \impl \Event p
\end{equation}

\spacer

\begin{equation}\label{E:IdemEvent}
\textbf{Absorption of $\Event$:}\quad \Event\Event p \equiv \Event p
\end{equation}

\spacer

\begin{equation}\label{E:dNextEvent}
\textbf{Exchange of $\Next$ and $\Event$:}\quad \Next\Event p \equiv \Event\Next p
\end{equation}

\spacer

\begin{equation}\label{E:distEventOr}
\textbf{Distributivity of $\Event$ over $\lor$:}\quad \Event(p \lor q) \equiv \Event p \lor \Event q
\end{equation}

\spacer

\begin{equation}\label{E:distEventAnd}
\textbf{Distributivity of $\Event$ over $\land$:}\quad \Event(p \land q) \impl \Event p \land \Event q
\end{equation}

\subsection*{Always $\quad\Always$}

\begin{equation}\label{E:defAlways}
\textbf{Definition of $\Always$:}\quad \Always p \equiv \neg\Event\neg p
\end{equation}

\firstspacer

\begin{equation}\label{E:induction}
\textbf{Axiom, Induction:}\quad \Always (p \impl \Next p) \impl (p \impl \Always p)
\end{equation}

\spacer

\begin{equation}\label{E:axiomAlwaysUntilImpl}
\textbf{Axiom, $\Until\Always$ implication:}\quad p\Until \Always q\impl \Always (p\Until q)
\end{equation}

\spacer

\begin{equation}\label{E:andUntilDist}
\textbf{Axiom, Distributivity of $\land$ over $\Until$:}\quad \Always p \land q \Until r \impl (p \land q) \Until (p \land r)
\end{equation}

\spacer

\begin{equation}\label{E:axAbsorpUntil}
\textbf{Absorption of $\Until$ into $\Always$:}\quad p \Until \Always p \equiv \Always p
\end{equation}

\spacer

\begin{equation}\label{E:axiomUntilImpl}
\textbf{$\Until$ implication:}\quad \Always p \land \Event q \impl p \Until q
\end{equation}

\spacer

\begin{equation}\label{E:eventAlwaysImp}
\textbf{$\Event \Always$ implication:}\quad \Event\Always p \impl \Always\Event p
\end{equation}

\spacer

\begin{equation}\label{E:eventAsAlways}
\Event p \equiv \neg\Always\neg p
\end{equation}

\spacer

\begin{equation}\label{E:dualAlways}
\textbf{Dual of $\Always$:}\quad \neg\Always p \equiv \Event\neg p
\end{equation}

\spacer

\begin{equation}\label{E:dualEvent}
\textbf{Dual of $\Event$:}\quad \neg\Event p \equiv \Always\neg p
\end{equation}

\spacer

\begin{equation}\label{E:alwaysTrue}
\textbf{Truth of $\Always$:}\quad \Always true \equiv true
\end{equation}

\spacer

\begin{equation}\label{E:alwaysFalse}
\textbf{Falsehood of $\Always$:}\quad \Always false \equiv false
\end{equation}

\spacer

\begin{equation}\label{E:expansionAlways}
\textbf{Expansion of $\Always$:}\quad \Always p \equiv p \land \Next\Always p
\end{equation}

\spacer

\begin{equation}\label{E:absAndIntoAlways}
\textbf{Absorption of $\land$ into $\Always$:}\quad p \land \Always p \equiv \Always p
\end{equation}

\spacer

\begin{equation}\label{E:absAlwaysIntoOr}
\textbf{Absorption of $\Always$ into $\lor$:}\quad \Always p \lor p \equiv p
\end{equation}

\spacer

\begin{equation}\label{E:absEventIntoAlways}
\textbf{Absorption of $\Event$ into $\Always$:}\quad \Event p \land \Always p \equiv \Always p
\end{equation}

\spacer

\begin{equation}\label{E:absAlwaysIntoEvent}
\textbf{Absorption of $\Always$ into $\Event$:}\quad \Always p \lor \Event p \equiv \Event p
\end{equation}

\spacer

\begin{equation}\label{E:IdemAlways}
\textbf{Absorption of $\Always$:}\quad \Always\Always p \equiv \Always p
\end{equation}

\newpage

\begin{equation}\label{E:dNextAlways}
\textbf{Exchange of $\Next$ and $\Always$:}\quad \Next\Always p \equiv \Always\Next p
\end{equation}

\spacer

\begin{equation}\label{E:impNext}
p \impl \Always p \equiv p \impl \Next\Always p
\end{equation}

\spacer

\begin{equation}\label{E:impAlways}
\textbf{Strengthening of $\Always$:}\quad \Always p \impl p
\end{equation}

\spacer

\begin{equation}\label{E:impAlwaysE}
\textbf{Strengthening of $\Always$:}\quad \Always p \impl \Event p
\end{equation}

\spacer

\begin{equation}\label{E:impAlwaysN}
\textbf{Strengthening of $\Always$:}\quad \Always p \impl \Next p
\end{equation}

\spacer

\begin{equation}\label{E:impAlwaysNA}
\textbf{Strengthening of $\Always$:}\quad \Always p \impl \Next\Always p
\end{equation}

\spacer

\begin{equation}\label{E:exAlwaysNot}
\textbf{Distributivity of $\neg$ over $\Always$:}\quad \Always\neg p \impl \neg\Always p
\end{equation}

\spacer

\begin{equation}\label{E:alwaysAndEvent}
\textbf{Distributivity of $\Event$ over $\land$:}\quad \Always p \land \Event q \impl \Event (p \land q)
\end{equation}

\spacer

\begin{equation}\label{E:excludedMid}
\textbf{Temporal excluded middle:}\quad \Event p \lor \Always\neg p
\end{equation}

\spacer

\begin{equation}\label{E:excludedMidb}
\textbf{Temporal excluded middle:}\quad \Always p \lor \Event\neg p
\end{equation}

\spacer

\begin{equation}\label{E:contradiction}
\textbf{Temporal contradiction:}\quad \Event p \land \Always\neg p \equivs false
\end{equation}

\spacer

\begin{equation}\label{E:contradictionb}
\textbf{Temporal contradiction:}\quad \Always p \land \Event\neg p \equivs false
\end{equation}

\spacer

\begin{equation}\label{E:distAlwaysAnd}
\textbf{Distributivity of $\Always$ over $\land$:}\quad \Always (p \land q) \equiv \Always p \land \Always q
\end{equation}

\spacer

\begin{equation}\label{E:distAlwaysOr}
\textbf{Distributivity of $\Always$ over $\lor$:}\quad (\Always p \lor \Always q) \impl \Always (p \lor q)
\end{equation}

\spacer

\begin{equation}\label{E:distAlwaysEquiv}
\textbf{Distributivity of $\Always$ over $\equiv$:}\quad \Always (p \equiv q) \impl (\Always p \equiv \Always q)
\end{equation}

\spacer

\begin{equation}\label{E:eventImpAlways}
\textbf{Distributivity of $\Event$ over $\impl$:}\quad \Event (p \impl q) \equiv (\Always p \impl \Event q)
\end{equation}

\spacer

\begin{equation}\label{E:eventPImplEventQ}
\textbf{Distributivity of $\Event$ over $\impl$:}\quad (\Event p \impl \Event q) \impl \Event (p \impl q)
\end{equation}

\spacer

\begin{equation}\label{E:alwaysImpNexts}
\textbf{Monotonicity of $\Next$:}\quad \Always (p \impl q) \impl (\Next p \impl \Next q)
\end{equation}

\spacer

\begin{equation}\label{E:alwaysImpEvents}
\textbf{Monotonicity of $\Event$:}\quad \Always (p \impl q) \impl (\Event p \impl \Event q)
\end{equation}

\spacer

\begin{equation}\label{E:distAlwaysImp}
\textbf{Monotonicity of $\Always$:}\quad \Always (p \impl q) \impl (\Always p \impl \Always q)
\end{equation}

\subsection*{Proof metatheorems}

\begin{equation}\label{E:metatheorem}
\textbf{Metatheorem:}\quad P \text{ is a theorem iff } \Always P \text{ is a theorem.}
\end{equation}

\firstspacer

\begin{equation}\label{E:metaEvent}
\textbf{Metatheorem $\Event$:}\quad \text{If } P\impl Q \text{ is a theorem then } \Event P\impl\Event Q \text{ is a theorem.}
\end{equation}

\spacer

\begin{equation}\label{E:metaAlways}
\textbf{Metatheorem $\Always$:}\quad \text{If } P\impl Q \text{ is a theorem then } \Always P\impl\Always Q \text{ is a theorem.}
\end{equation}

\subsection*{Always, continued}

\begin{equation}\label{E:distAlwaysEventAnd}
\textbf{Distributivity of $\Always\Event$ over $\land$:}\quad \Always\Event(p \land q) \impl \Always\Event p \land \Always\Event q
\end{equation}

\firstspacer

\begin{equation}\label{E:distEventAlwaysOr}
\textbf{Distributivity of $\Event\Always$ over $\lor$:}\quad \Event\Always p \lor \Event\Always q \impl \Event\Always (p \lor q)
\end{equation}

\spacer

\begin{equation}\label{E:distAlwaysEventOr}
\textbf{Distributivity of $\Always\Event$ over $\lor$:}\quad \Always\Event(p \lor q) \equiv \Always\Event p \lor \Always\Event q
\end{equation}

\spacer

\begin{equation}\label{E:distEventAlwaysAnd}
\textbf{Distributivity of $\Event\Always$ over $\land$:}\quad \Event\Always(p \land q) \equiv \Event\Always p \land \Event\Always q
\end{equation}

\spacer

\begin{equation}\label{E:absEvent}
\textbf{Absorption of $\Event$ into $\Always\Event$:}\quad \Event\Always\Event p \equiv \Always\Event p
\end{equation}

\spacer

\begin{equation}\label{E:absAlways}
\textbf{Absorption of $\Always$ into $\Event\Always$:}\quad \Always\Event\Always p \equiv \Event\Always p
\end{equation}

\spacer

\begin{equation}\label{E:eventAlwaysPAndAlwaysEventQ}
\Event\Always p\land \Always\Event q \impl \Always\Event (p\land q)
\end{equation}

\spacer

\begin{equation}\label{E:PrProofRule}
\textbf{Progress proof rule:}\quad \Event\Always p \land \Always(\Always p \impl \Event q) \impl \Event q
\end{equation}
\newpage

\subsection*{Wait $\quad\Wait$}

\begin{equation}\label{E:defWait}
\textbf{Definition of $\Wait$:}\quad p \Wait q \equiv \Always p\lor p \Until q
\end{equation}

\firstspacer

\begin{equation}\label{E:notWait}
\textbf{Axiom, Distributivity of $\neg$ over $\Wait$:}\quad \neg (p \Wait q) \equiv \neg q \Until (\neg p \land \neg q)
\end{equation}

\spacer

\begin{equation}\label{E:untilFromWait}
\textbf{$\Until$ in terms of $\Wait$:}\quad p \Until q \equiv p \Wait q\land \Event q
\end{equation}

\spacer

\begin{equation}\label{E:notUntil}
\textbf{Distributivity of $\neg$ over $\Until$:}\quad \neg (p \Until q) \equiv \neg q \Wait (\neg p \land \neg q)
\end{equation}

\spacer

\begin{equation}\label{untilImplWait}
p\Until q\impl p\Wait q
\end{equation}

\spacer

\begin{equation}\label{E:andWaitDist}
\textbf{Distributivity of $\land$ over $\Wait$:}\quad \Always p \land q \Wait r \impl (p \land q) \Wait (p \land r)
\end{equation}

\spacer

\begin{equation}\label{E:alwaysImpWait}
\textbf{Perpetuity:}\quad \Always p \impl p \Wait q
\end{equation}

\spacer

\begin{equation}\label{E:waitNextDist}
\textbf{Distributivity of $\Next$ over $\Wait$:}\quad \Next (p \Wait q) \equiv \Next p \Wait \Next q
\end{equation}

\spacer

\begin{equation}\label{E:expansionWait}
\textbf{Expansion of $\Wait$:}\quad p \Wait q \equiv q \lor (p \land \Next (p \Wait q))
\end{equation}

\spacer

\begin{equation}\label{E:waitExcludedMiddle}
\Wait \textbf{excluded middle:}\quad p \Wait q \lor p\Wait \neg q
\end{equation}

\spacer

\begin{equation}\label{E:leftZeroWait}
\textbf{Left zero of $\Wait$:}\quad true \Wait q \equiv true
\end{equation}

\spacer

\begin{equation}\label{E:waitOrDist}
\textbf{Left distributivity of $\Wait$ over $\lor$:}\quad p \Wait (q \lor r) \equiv p \Wait q \lor p \Wait r
\end{equation}

\spacer

\begin{equation}\label{E:rightWaitOrDist}
\textbf{Right distributivity of $\Wait$ over $\lor$:}\quad p \Wait r \lor q \Wait r \impl (p \lor q) \Wait r
\end{equation}

\spacer

\begin{equation}\label{E:leftWaitAndDist}
\textbf{Left distributivity of $\Wait$ over $\land$:}\quad p \Wait (q \land r) \impl p \Wait q \land p \Wait r
\end{equation}

\spacer

\begin{equation}\label{E:rightWaitAndDist}
\textbf{Right distributivity of $\Wait$ over $\land$}\quad (p \land q) \Wait r\equiv p \Wait r \land q \Wait r
\end{equation}

\spacer

\begin{equation}\label{E:disjunctWait}
\textbf{Disjunction rule of $\Wait$:}\quad p\Wait q\equiv (p\lor q)\Wait q
\end{equation}

\spacer

\begin{equation}\label{E:disjunctUntil}
\textbf{Disjunction rule of $\Until$:}\quad p\Until q\equiv (p\lor q)\Until q
\end{equation}

\spacer

\begin{equation}\label{E:ruleWait}
\textbf{Rule of $\Wait$:}\quad \neg q \Wait q
\end{equation}

\spacer

\begin{equation}\label{E:ruleUntil}
\textbf{Rule of $\Until$:}\quad \neg q \Until q\equivs \Event q
\end{equation}

\spacer

\begin{equation}\label{E:pImplQWaitP}
(p\impl q)\Wait p
\end{equation}

\spacer

\begin{equation}\label{E:eventPImplPImplUntilp}
\Event p\impl(p\impl q)\Until p
\end{equation}

\spacer

\begin{equation}\label{E:conRuleWait}
\textbf{Conjunction rule of $\Wait$:}\quad p\Wait q\equiv (p\land \neg q)\Wait q
\end{equation}

\spacer

\begin{equation}\label{E:conRuleUntil}
\textbf{Conjunction rule of $\Until$:}\quad p\Until q\equiv (p\land \neg q)\Until q
\end{equation}

\spacer

\begin{equation}\label{E:notWait2}
\textbf{Distributivity of $\neg$ over $\Wait$:}\quad \neg(p\Wait q)\equiv (p\land \neg q)\Until(\neg p\land \neg q)
\end{equation}

\spacer

\begin{equation}\label{E:notUntil2}
\textbf{Distributivity of $\neg$ over $\Until$:}\quad \neg(p\Until q)\equiv (p\land \neg q)\Wait(\neg p\land \neg q)
\end{equation}

\spacer

\begin{equation}\label{E:idempWait}
\textbf{Idempotency of $\Wait$:}\quad p \Wait p \equiv p
\end{equation}

\spacer

\begin{equation}\label{E:rightZeroWait}
\textbf{Right zero of $\Wait$:}\quad p \Wait true \equiv true
\end{equation}

\spacer

\begin{equation}\label{E:leftIdentWait}
\textbf{Left identity of $\Wait$:}\quad false \Wait q \equiv q
\end{equation}

\spacer

\begin{equation}\label{E:waitToOr}
p \Wait q \impl p \lor q
\end{equation}

\spacer

\begin{equation}\label{E:orToWait}
\Always (p\lor q) \impl p \Wait q
\end{equation}

\spacer

\begin{equation}\label{E:waitInsertion}
\textbf{Insertion:}\quad q \impl p \Wait q
\end{equation}

\newpage

\begin{equation}\label{E:waitOrP}
\textbf{Absorption:}\quad p\lor p\Wait q\equiv p\lor q
\end{equation}

\spacer

\begin{equation}\label{E:waitOrQ}
\textbf{Absorption:}\quad p\Wait q\lor q\equiv p\Wait q
\end{equation}

\spacer

\begin{equation}\label{E:waitAndQ}
\textbf{Absorption:}\quad p\Wait q\land q\equiv q
\end{equation}

\spacer

\begin{equation}\label{E:waitAndOr}
\textbf{Absorption:}\quad p\Wait q\land (p\lor q) \equiv p\Wait q
\end{equation}

\spacer

\begin{equation}\label{E:waitOrAnd}
\textbf{Absorption:}\quad p\Wait q\lor (p\land q) \equiv p\Wait q
\end{equation}

\spacer

\begin{equation}\label{E:waitAbsL}
\textbf{Left absorption of $\Wait$:}\quad p \Wait (p \Wait q) \equiv p \Wait q
\end{equation}

\spacer

\begin{equation}\label{E:waitAbsR}
\textbf{Right absorption of $\Wait$:}\quad (p \Wait q) \Wait q \equiv p \Wait q
\end{equation}

\spacer

\begin{equation}\label{E:alwaysAsWait}
\Always p \equiv p \Wait false
\end{equation}

\spacer

\begin{equation}\label{E:waitEntailment}
\textbf{$\Wait$ implication:}\quad p \Wait q \impl \Always p\lor \Event q
\end{equation}

\spacer

\begin{equation}\label{E:leftWaitAbsUtil}
\textbf{Absorption:}\quad p \Wait (p \Until q) \equiv p \Wait q
\end{equation}

\spacer

\begin{equation}\label{E:rightWaitAbsUtil}
\textbf{Absorption:}\quad (p \Until q) \Wait q \equiv p \Until q
\end{equation}

\spacer

\begin{equation}\label{E:leftUntilAbsWait}
\textbf{Absorption:}\quad p \Until (p \Wait q) \equiv p \Wait q
\end{equation}

\spacer

\begin{equation}\label{E:rightUntilAbsWait}
\textbf{Absorption:}\quad (p \Wait q) \Until q \equiv p \Until q
\end{equation}

\spacer

\begin{equation}\label{E:absorpEventWait}
\textbf{Absorption of $\Wait$ into $\Event$:}\quad \Event q \Wait q \equiv \Event q
\end{equation}

\spacer

\begin{equation}\label{E:absWaitAlways}
\textbf{Absorption of $\Wait$ into $\Always$:}\quad \Always p\land p\Wait q\equiv \Always p
\end{equation}

\spacer

\begin{equation}\label{E:absAlwaysWait}
\textbf{Absorption of $\Always$ into $\Wait$:}\quad \Always p\lor p\Wait q\equiv p\Wait q
\end{equation}

\spacer

\begin{equation}\label{E:waitEntailAlways}
p \Wait q \land \Always\neg q \impl \Always p
\end{equation}

\spacer

\begin{equation}\label{E:untilEntailAlways}
\Always p\impl p \Until q \lor \Always\neg q 
\end{equation}

\spacer

\begin{equation}\label{E:waitEntailEvent}
\neg\Always p\land p \Wait q \impl \Event q
\end{equation}

\spacer

\begin{equation}\label{E:untilEntailEvent}
\Event q\impl \neg\Always p\lor p \Until q 
\end{equation}

\spacer

\begin{equation}\label{E:rightMonoUntil}
\textbf{Right monotonicity of $\Until$:}\quad \Always (p \impl q) \impl (r \Until p \impl r \Until q)
\end{equation}

\spacer

\begin{equation}\label{E:leftMonoWait}
\textbf{Left monotonicity of $\Wait$:}\quad \Always (p \impl q) \impl (p \Wait r \impl q \Wait r)
\end{equation}

\spacer

\begin{equation}\label{E:leftMonoUntil}
\textbf{Left monotonicity of $\Until$:}\quad \Always (p \impl q) \impl (p \Until r \impl q \Until r)
\end{equation}

\spacer

\begin{equation}\label{E:rightMonoWait}
\textbf{Right monotonicity of $\Wait$:}\quad \Always (p \impl q) \impl (r \Wait p \impl r \Wait q)
\end{equation}

\spacer

\begin{equation}\label{E:waitImpAbsR}
\textbf{Absorption:}\quad (p \Wait q) \Wait r \impl (p \lor q) \Wait r
\end{equation}

\spacer

\begin{equation}\label{E:waitImpAbsL}
\textbf{Absorption:}\quad p \Wait (q \Wait r) \impl (p \lor q) \Wait r \quad [\textit{Not yet proved.}]
\end{equation}

\spacer

\begin{equation}\label{E:waitOrderingThree}
\textbf{Ordering:}\quad p \Wait (q \land r) \impl (p \Wait q) \Wait r \quad [\textit{Not yet proved.}]
\end{equation}

\spacer

\begin{equation}\label{E:waitOrdering}
\textbf{Ordering:}\quad \neg p \Wait q \lor \neg q \Wait p
\end{equation}

\spacer

\begin{equation}\label{E:waitOrderingTwo}
\textbf{Ordering:}\quad \Always (p \Wait q \land \neg q \Wait r) \impl p \Wait r
\end{equation}

\end{document}